COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 caroly.lsp[f81,jmc]	ekl version of Carolyn's recursive function maker
C00004 ENDMK
C⊗;
;;; caroly.lsp[f81,jmc]	ekl version of Carolyn's recursive function maker
;;; see bm[grt,clt]

(declare (u u0 u1 u2 v v0 v1 v2) list)

(declare (g g0 g1) |ground→ground|)

(declare f |((ground→ground)→ground)⊗ground→ground|)

(declare (cvil) |(ground→ground)⊗(N⊗N→truthval)⊗(ground→N)⊗ground| constant)

(declare wfo |(ground⊗ground→truthval)→truthval| constant)

(declare listfn |(ground→ground)→truthval| const)

(axiom |∀g.listfn(g) ⊃ ∀u.list(g(u))|)

(declare bottom ground constant)

(declare rank |ground→N|)

(declare << |N⊗N→truthval|)

(axiom |(cvil(g,<<,rank,x,bottom))(y) = if rank(y) << rank(x) then g(y)
else bottom|)

(axiom |∀<<.wfo(<<) ⊃ ∀x.boyermoore(f)(x) = f(cvi(boyermoore(f),<<,rho,x),x)|)